package ch.epfl.lara.matcheck.verify.spec;

import ch.epfl.lara.matcheck.ast._
import ch.epfl.lara.matcheck.util.Substitute
import ch.epfl.lara.matcheck.verify.provers.ProverResults
import ch.epfl.lara.matcheck.types._
import ch.epfl.lara.matcheck.ast.parser.Desugar

object MethodSpecVerifier extends SpecVerifier {
  import ch.epfl.lara.matcheck.verify.transform.{TreeExpr2Formula,Pattern2Formula}
  
  implicit def string2element(name: String): Element = Element(name)
  
  def apply(method: MethodDef): Unit = {
    val MethodDef(name,params,returnType,ppc,body) = method
    val (pre,post) = ppc match {
      case None  => (Tru,Tru)
      case Some((pre,post)) => (pre,post)
    }
    
    val params_axioms = params.foldLeft[Formula](Tru)((acc,param) => {
    		            val ParamDef(name,tpe) = param
                            var param_formula: Formula = Tru
                            if(name.sym != null) {
                              name.sym.getTpe match {
                                case IClassType(c) => 
                                  param_formula = Substitute("this",name.getName,c.invariant.getOrElse(Tru))
                                case _ => ()
                              }
                            }
                            And(And(In(param.getName,TreeExpr2Formula(param.tpe)),param_formula),acc)
    })    
    
    val return_tpe = returnType match {
      case OptionType(xs) if !xs.isEmpty =>
        val results = List.range(1,xs.length+1).map(i => "res"+i)
        results.zip(xs).foldLeft[Formula](Tru)({case (acc,(name,tpe)) => And(In(name,Set(tpe.toString)),acc)})
      case tpe => In("res",Set(tpe.toString)) 
    }
      
    val method_axioms = And(And(params_axioms,return_tpe),pre)
    
    val body2formula = Body2Formula(method_axioms,method.name.sym.RES,body)
    
    val f = Imply(And(method_axioms,body2formula),
                  post)
    
    provePostcondition(method.name.sym, f)
  }
  
  override protected def startTimer() {
    Timer.startProvingPostcondition()
  }
  
  override protected def stopTimer() {
    Timer.finishedProvingPostcondition()
  }
  
  
  override def prove(f: Formula): ProverResults.ProverResult = {
    super.prove(Imply(AxiomsHolder.axioms,f))
  }
  
  private def proveInvariant(ts: TypeSymbol, f: Formula) {
    val result = prove(f)
    debug("invariant",None, ts, result)
  }  
    
  private def provePrecondition(m: MethodSymbol, f: Formula) {
    val result = prove(f)
    debug("precondition",Some(m.getName), m.name.getSym, result)
  }
  
  private def provePostcondition(m: MethodSymbol, f: Formula) {
    val result = prove(f)
    debug("postcondition",Some(m.getName), m.name.getSym, result)
  }
  
  private def debug(wrong: String, method: Option[String], cont: TypeSymbol, result: ProverResults.ProverResult) {
    val container = (cont: @unchecked) match {
      case c: ClassSymbol => " in class " + c.getName 
      case o: ObjectSymbol => " in object " + o.getName
    }
    
    val methodOut = method match {
      case None => ""
      case Some(m) => " of method " + m
    }
    
    result match {
      case ProverResults.Valid => 
        Report.verbose(wrong + methodOut + container + " is valid.")
      case ProverResults.Timeout =>
        Report.error(wrong + methodOut + container + " couldn't be verified. Prover Timeout.")
      case ProverResults.Invalid =>
        Report.error(wrong + methodOut + container + " is invalid.")
    }
    super.debug(last_formula_proved)
  }
  
  
  private object Body2Formula  {
    
    private def freshName(name: String): String  = {
      import ch.epfl.lara.matcheck.util.FreshName
      FreshName.fresh(name)
    }
    
   
    
    def apply(axiom: Formula, result: String, expr: Expr): Formula = {
      var _local_formula: Formula = Tru
      def local_formula(f: Formula): Unit = _local_formula = And(_local_formula,f)
      def local_axioms = And(axiom,_local_formula)
      
      def packBoolBinOp[S<:Formula](op: (E,E)=>S, left: Expr, right: Expr): Formula = {
        val res_left = freshName("left")
        val res_right = freshName("right")
        local_formula(this(local_axioms,res_left,left))
        local_formula(this(local_axioms,res_right,right))
        local_formula(pack(op(res_left,res_right)))
        _local_formula
      }
    
      def packArithBinOp(op: (Term0,Term0)=>Term0, left: Expr, right: Expr): Formula = {
        val res_left = freshName("left")
        val res_right = freshName("right")
        local_formula(this(local_axioms,res_left,left))
        local_formula(this(local_axioms,res_right,right))
        local_formula(pack(op(IntVar(res_left),IntVar(res_right))))
        _local_formula
      }
      
      def pack(f: Formula): Formula = Equality(result,f)
      
      expr match {
        case ObjectId(name) => 
          val static_name = "object__"+name.getName
          Eq(result,static_name)
        
        case Ident(name) if name.getName == Constants.NONE => 
          And(Eq(result,"res"),Eq("res",name.getName))
          
        case Ident(name)  => pack(Element(name.getName)) 
        case True         => pack(Tru)
        case False        => pack(Flse)
        case Number(n)    => pack(Const(n)) 
        case StringLit(s) => pack(StringLit0(s))
        
        case IsInstanceOf(e,tpe) =>
          val isinstof = freshName("isinstof")
          local_formula(this(local_axioms,isinstof,e))
          local_formula(Equality(result,In(isinstof,TreeExpr2Formula(tpe))))
          _local_formula
        
        case New(klass,args) =>
          val xs: List[String] = for(arg<-args) yield {
            val fresh_arg = freshName("arg")
            local_formula(this(local_axioms,fresh_arg,arg))
            fresh_arg
          }
          
          for((field,value)<-klass.getSym.allFields.zip(xs)) {
            val name = klass.getName + "_getField_" +field.getName
            local_formula(Eq(Function(name,List(result)),value))
          }
        
          klass.getSym.invariant match {
            case None => ()
            case Some(inv) =>
              val invariant = Substitute("this",result,inv);
              proveInvariant(klass.getSym,Imply(local_axioms,invariant))
              local_formula(invariant)
          }

          local_formula(In(result,Set(klass.getName)))
          _local_formula
          
        case Call(ObjectId(name),_,args) if name.getName == Constants.SOME =>
          args(0) match {
            case Call(_,_,results) => 
              for(i<-List.range(0,results.length))  {
                local_formula(this(local_axioms,"res"+(i+1),results(i)))
              }
            case arg => local_formula(this(local_axioms,"res1",arg))
          }

          _local_formula
        
        case Call(obj,method,args) =>
          val this_name = freshName("this_obj")
          local_formula(this(local_axioms,this_name,obj))

          val args_fresh = for(arg<-args) yield {
            val a_fresh = freshName("arg")
            local_formula(this(local_axioms,a_fresh,arg))        
            a_fresh
          }

          
    
          if(method.getSym != null) {
            val msym @ MethodSymbol(mname,params,retTpe,ppc) = method.getSym
            var env = ("this",this_name) ::  params.map(_._1).zip(args_fresh)
            
            val precondition = ppc match {
              case None => Tru
              case Some((pre,_)) => pre
            }
            provePrecondition(msym,Imply(local_axioms,Substitute(env,precondition)))
            
            val name = mname.getSym.getName+"_"+mname
  
            env = (msym.RES,result) :: env
  
            val postcondition = ppc match {
              case None => Tru
              case Some((_,post)) => Substitute(env,post) 
            }
            local_formula(postcondition)
            
            retTpe match {
              case IClassType(c) => local_formula(In(result,Set(c.getName)))
              case _ => ()
            }
            
            local_formula(Eq(result,Function(name,this_name :: args_fresh.map(Element(_)))))
          } else {
            var name: String = method.getName+freshName(method.getName)
            local_formula(Eq(result,name))
          }
    
    
          _local_formula
        
        case Select(obj,field) =>
          val this_res = freshName("this_obj")
          local_formula(this(local_axioms,this_res,obj))
          
          if(field.getSym != null) {
            val name = field.getSym.name.getSym.getName+"_getField_"+field.getName
            local_formula(Eq(Function(name,List(this_res)),result))
          } 
          _local_formula
        
        case &&(left,right) => packBoolBinOp(And , left, right)
        case ||(left,right) => packBoolBinOp(Or , left, right)  
        case +(left,right) => packArithBinOp(Plus , left,right)
        case -(left,right) => packArithBinOp(Minus , left,right)  
        case /(left,right) => packArithBinOp(Div , left,right)
        case %(left,right) => packArithBinOp(Mod , left,right)
        case *(left,right) => packArithBinOp(Prod , left,right)
        case <(left,right)  => packBoolBinOp(Less ,left,right)
        case <=(left,right) => packBoolBinOp(LessEq ,left,right)
        case ==(left,right) => packBoolBinOp(Eq ,left,right)
        case !(f) => 
          val neg = freshName("neg")
          local_formula(this(local_axioms,neg,f))
          local_formula(Equality(result,Neg(neg)))
          _local_formula
          
        case If(cond,then,elze) =>
          val cond_res = freshName("cond_res")
          val then_res = freshName("then_res")
          val elze_res = freshName("elze_res")
          local_formula( this(local_axioms,cond_res,cond) ) 
          local_formula(Imply(And(cond_res,Eq(result,then_res)),this(And(local_axioms,cond_res),then_res,then)))
          local_formula(Imply(And(Neg(cond_res),Eq(result,elze_res)),this(And(local_axioms,Neg(cond_res)),elze_res,elze)))
          _local_formula 
      
          
        case Match(scrutinee,tpe,cases) =>
          val res_scrutinee = freshName("scrutinee")
          local_formula(this(local_axioms,res_scrutinee,scrutinee))
          local_formula(In(res_scrutinee,TreeExpr2Formula(tpe)))
          
         
          val cases2formula = for(CaseDef(pos,pattern,guard,body)<-cases) yield {
          
            val Imply(p_lhs,p_rhs) = Pattern2Formula(res_scrutinee,pattern)
            var pattern2formula: Formula = And(p_lhs,p_rhs)
            
            if(guard.isDefined) {
              val guard_res = freshName("guard_res"+pos)
              pattern2formula = And(pattern2formula,
                                    this(And(local_axioms,pattern2formula),
                                             guard_res,guard.get))
              pattern2formula = And(pattern2formula,guard_res)
            }
            
            val body_res = freshName("body_res"+pos)
            And(And(pattern2formula,Eq(result,body_res)),
                      this(And(local_axioms,And(pattern2formula,Eq(result,body_res))),body_res,body))
          }
          
          var pm: Formula = Tru
          if(cases2formula.length < 2) () 
          else for(i<-List.range(0,cases2formula.length-1);j<-List.range(i+1,cases2formula.length)) {
            pm = And(pm,Neg(And(cases2formula(i),cases2formula(j))))  
          }
          
          And(pm,
              cases2formula.foldLeft[Formula](Flse)((l,r) => Or(l,r)))
          
      }
      
    }
    
  
  }  
  
}
